Nuprl Lemma : conditional_wf
11,40
postcript
pdf
T
,
V
:Type,
A
:(
T
),
dcd_A
:(
t
:
T
Dec(
A
(
t
))),
f
:({
t
:
T
|
A
(
t
)}
V
),
g
:({
t
:
T
|
(
A
(
t
))}
V
).
[
A
?
f
:
g
]
T
V
latex
Definitions
t
T
,
left
+
right
,
P
Q
,
Dec(
P
)
,
x
:
A
B
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
s
=
t
,
,
f
(
a
)
,
if
p
:
P
then
A
(
p
) else
B
fi
,
x
.
A
(
x
)
,
[
P
?
f
:
g
]
,
A
,
{
x
:
A
|
B
(
x
)}
,
Type
origin
T, V:Type, A:(T
), dcd_A:(t:TDec(A(t))), f:({t:T| A(t)} V), g:({t:T| 
(A(t))} V).
TV T, V:Type, A:(T), dcd_A:(t:TDec(A(t))), f:({t:T| A(t)} V), g:({t:T| (A(t))} V).
TV T
QB(x)
Qx:A. B(x)
x.A(x)A